$\forall$$A$,$B$:Type, $x$:($A$ + $B$). ($\uparrow$isl($x$)) $\Rightarrow$ (outl($x$) $\in$ $A$)